(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
f(a(x), y, s(z), u) → f(a(b), y, z, g(x, y, s(z), u))
g(x, y, z, u) → h(x, y, z, u)
h(b, y, z, u) → f(y, y, z, u)
a(b) → c
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a(z0), z1, s(z2), z3) → f(a(b), z1, z2, g(z0, z1, s(z2), z3))
g(z0, z1, z2, z3) → h(z0, z1, z2, z3)
h(b, z0, z1, z2) → f(z0, z0, z1, z2)
a(b) → c
Tuples:
F(a(z0), z1, s(z2), z3) → c1(F(a(b), z1, z2, g(z0, z1, s(z2), z3)), A(b), G(z0, z1, s(z2), z3))
G(z0, z1, z2, z3) → c2(H(z0, z1, z2, z3))
H(b, z0, z1, z2) → c3(F(z0, z0, z1, z2))
S tuples:
F(a(z0), z1, s(z2), z3) → c1(F(a(b), z1, z2, g(z0, z1, s(z2), z3)), A(b), G(z0, z1, s(z2), z3))
G(z0, z1, z2, z3) → c2(H(z0, z1, z2, z3))
H(b, z0, z1, z2) → c3(F(z0, z0, z1, z2))
K tuples:none
Defined Rule Symbols:
f, g, h, a
Defined Pair Symbols:
F, G, H
Compound Symbols:
c1, c2, c3
(3) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a(z0), z1, s(z2), z3) → f(a(b), z1, z2, g(z0, z1, s(z2), z3))
g(z0, z1, z2, z3) → h(z0, z1, z2, z3)
h(b, z0, z1, z2) → f(z0, z0, z1, z2)
a(b) → c
Tuples:
G(z0, z1, z2, z3) → c2(H(z0, z1, z2, z3))
H(b, z0, z1, z2) → c3(F(z0, z0, z1, z2))
F(a(z0), z1, s(z2), z3) → c1(F(a(b), z1, z2, g(z0, z1, s(z2), z3)), G(z0, z1, s(z2), z3))
S tuples:
G(z0, z1, z2, z3) → c2(H(z0, z1, z2, z3))
H(b, z0, z1, z2) → c3(F(z0, z0, z1, z2))
F(a(z0), z1, s(z2), z3) → c1(F(a(b), z1, z2, g(z0, z1, s(z2), z3)), G(z0, z1, s(z2), z3))
K tuples:none
Defined Rule Symbols:
f, g, h, a
Defined Pair Symbols:
G, H, F
Compound Symbols:
c2, c3, c1
(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
a(
z0),
z1,
s(
z2),
z3) →
c1(
F(
a(
b),
z1,
z2,
g(
z0,
z1,
s(
z2),
z3)),
G(
z0,
z1,
s(
z2),
z3)) by
F(a(z0), z1, s(x2), z3) → c1(F(a(b), z1, x2, h(z0, z1, s(x2), z3)), G(z0, z1, s(x2), z3))
F(a(x0), x1, s(x2), x3) → c1(F(c, x1, x2, g(x0, x1, s(x2), x3)), G(x0, x1, s(x2), x3))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a(z0), z1, s(z2), z3) → f(a(b), z1, z2, g(z0, z1, s(z2), z3))
g(z0, z1, z2, z3) → h(z0, z1, z2, z3)
h(b, z0, z1, z2) → f(z0, z0, z1, z2)
a(b) → c
Tuples:
G(z0, z1, z2, z3) → c2(H(z0, z1, z2, z3))
H(b, z0, z1, z2) → c3(F(z0, z0, z1, z2))
F(a(z0), z1, s(x2), z3) → c1(F(a(b), z1, x2, h(z0, z1, s(x2), z3)), G(z0, z1, s(x2), z3))
F(a(x0), x1, s(x2), x3) → c1(F(c, x1, x2, g(x0, x1, s(x2), x3)), G(x0, x1, s(x2), x3))
S tuples:
G(z0, z1, z2, z3) → c2(H(z0, z1, z2, z3))
H(b, z0, z1, z2) → c3(F(z0, z0, z1, z2))
F(a(z0), z1, s(x2), z3) → c1(F(a(b), z1, x2, h(z0, z1, s(x2), z3)), G(z0, z1, s(x2), z3))
F(a(x0), x1, s(x2), x3) → c1(F(c, x1, x2, g(x0, x1, s(x2), x3)), G(x0, x1, s(x2), x3))
K tuples:none
Defined Rule Symbols:
f, g, h, a
Defined Pair Symbols:
G, H, F
Compound Symbols:
c2, c3, c1
(7) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a(z0), z1, s(z2), z3) → f(a(b), z1, z2, g(z0, z1, s(z2), z3))
g(z0, z1, z2, z3) → h(z0, z1, z2, z3)
h(b, z0, z1, z2) → f(z0, z0, z1, z2)
a(b) → c
Tuples:
G(z0, z1, z2, z3) → c2(H(z0, z1, z2, z3))
H(b, z0, z1, z2) → c3(F(z0, z0, z1, z2))
F(a(z0), z1, s(x2), z3) → c1(F(a(b), z1, x2, h(z0, z1, s(x2), z3)), G(z0, z1, s(x2), z3))
F(a(x0), x1, s(x2), x3) → c1(G(x0, x1, s(x2), x3))
S tuples:
G(z0, z1, z2, z3) → c2(H(z0, z1, z2, z3))
H(b, z0, z1, z2) → c3(F(z0, z0, z1, z2))
F(a(z0), z1, s(x2), z3) → c1(F(a(b), z1, x2, h(z0, z1, s(x2), z3)), G(z0, z1, s(x2), z3))
F(a(x0), x1, s(x2), x3) → c1(G(x0, x1, s(x2), x3))
K tuples:none
Defined Rule Symbols:
f, g, h, a
Defined Pair Symbols:
G, H, F
Compound Symbols:
c2, c3, c1, c1
(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
a(
z0),
z1,
s(
x2),
z3) →
c1(
F(
a(
b),
z1,
x2,
h(
z0,
z1,
s(
x2),
z3)),
G(
z0,
z1,
s(
x2),
z3)) by
F(a(x0), x1, s(x2), x3) → c1(F(c, x1, x2, h(x0, x1, s(x2), x3)), G(x0, x1, s(x2), x3))
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a(z0), z1, s(z2), z3) → f(a(b), z1, z2, g(z0, z1, s(z2), z3))
g(z0, z1, z2, z3) → h(z0, z1, z2, z3)
h(b, z0, z1, z2) → f(z0, z0, z1, z2)
a(b) → c
Tuples:
G(z0, z1, z2, z3) → c2(H(z0, z1, z2, z3))
H(b, z0, z1, z2) → c3(F(z0, z0, z1, z2))
F(a(x0), x1, s(x2), x3) → c1(G(x0, x1, s(x2), x3))
F(a(x0), x1, s(x2), x3) → c1(F(c, x1, x2, h(x0, x1, s(x2), x3)), G(x0, x1, s(x2), x3))
S tuples:
G(z0, z1, z2, z3) → c2(H(z0, z1, z2, z3))
H(b, z0, z1, z2) → c3(F(z0, z0, z1, z2))
F(a(x0), x1, s(x2), x3) → c1(G(x0, x1, s(x2), x3))
F(a(x0), x1, s(x2), x3) → c1(F(c, x1, x2, h(x0, x1, s(x2), x3)), G(x0, x1, s(x2), x3))
K tuples:none
Defined Rule Symbols:
f, g, h, a
Defined Pair Symbols:
G, H, F
Compound Symbols:
c2, c3, c1, c1
(11) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a(z0), z1, s(z2), z3) → f(a(b), z1, z2, g(z0, z1, s(z2), z3))
g(z0, z1, z2, z3) → h(z0, z1, z2, z3)
h(b, z0, z1, z2) → f(z0, z0, z1, z2)
a(b) → c
Tuples:
G(z0, z1, z2, z3) → c2(H(z0, z1, z2, z3))
H(b, z0, z1, z2) → c3(F(z0, z0, z1, z2))
F(a(x0), x1, s(x2), x3) → c1(G(x0, x1, s(x2), x3))
S tuples:
G(z0, z1, z2, z3) → c2(H(z0, z1, z2, z3))
H(b, z0, z1, z2) → c3(F(z0, z0, z1, z2))
F(a(x0), x1, s(x2), x3) → c1(G(x0, x1, s(x2), x3))
K tuples:none
Defined Rule Symbols:
f, g, h, a
Defined Pair Symbols:
G, H, F
Compound Symbols:
c2, c3, c1
(13) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use instantiation to replace
G(
z0,
z1,
z2,
z3) →
c2(
H(
z0,
z1,
z2,
z3)) by
G(x0, x1, s(x2), x3) → c2(H(x0, x1, s(x2), x3))
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a(z0), z1, s(z2), z3) → f(a(b), z1, z2, g(z0, z1, s(z2), z3))
g(z0, z1, z2, z3) → h(z0, z1, z2, z3)
h(b, z0, z1, z2) → f(z0, z0, z1, z2)
a(b) → c
Tuples:
H(b, z0, z1, z2) → c3(F(z0, z0, z1, z2))
F(a(x0), x1, s(x2), x3) → c1(G(x0, x1, s(x2), x3))
G(x0, x1, s(x2), x3) → c2(H(x0, x1, s(x2), x3))
S tuples:
H(b, z0, z1, z2) → c3(F(z0, z0, z1, z2))
F(a(x0), x1, s(x2), x3) → c1(G(x0, x1, s(x2), x3))
G(x0, x1, s(x2), x3) → c2(H(x0, x1, s(x2), x3))
K tuples:none
Defined Rule Symbols:
f, g, h, a
Defined Pair Symbols:
H, F, G
Compound Symbols:
c3, c1, c2
(15) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use instantiation to replace
H(
b,
z0,
z1,
z2) →
c3(
F(
z0,
z0,
z1,
z2)) by
H(b, x1, s(x2), x3) → c3(F(x1, x1, s(x2), x3))
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a(z0), z1, s(z2), z3) → f(a(b), z1, z2, g(z0, z1, s(z2), z3))
g(z0, z1, z2, z3) → h(z0, z1, z2, z3)
h(b, z0, z1, z2) → f(z0, z0, z1, z2)
a(b) → c
Tuples:
F(a(x0), x1, s(x2), x3) → c1(G(x0, x1, s(x2), x3))
G(x0, x1, s(x2), x3) → c2(H(x0, x1, s(x2), x3))
H(b, x1, s(x2), x3) → c3(F(x1, x1, s(x2), x3))
S tuples:
F(a(x0), x1, s(x2), x3) → c1(G(x0, x1, s(x2), x3))
G(x0, x1, s(x2), x3) → c2(H(x0, x1, s(x2), x3))
H(b, x1, s(x2), x3) → c3(F(x1, x1, s(x2), x3))
K tuples:none
Defined Rule Symbols:
f, g, h, a
Defined Pair Symbols:
F, G, H
Compound Symbols:
c1, c2, c3
(17) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use instantiation to replace
F(
a(
x0),
x1,
s(
x2),
x3) →
c1(
G(
x0,
x1,
s(
x2),
x3)) by
F(a(z0), a(z0), s(x1), x2) → c1(G(z0, a(z0), s(x1), x2))
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a(z0), z1, s(z2), z3) → f(a(b), z1, z2, g(z0, z1, s(z2), z3))
g(z0, z1, z2, z3) → h(z0, z1, z2, z3)
h(b, z0, z1, z2) → f(z0, z0, z1, z2)
a(b) → c
Tuples:
F(a(x0), x1, s(x2), x3) → c1(G(x0, x1, s(x2), x3))
G(x0, x1, s(x2), x3) → c2(H(x0, x1, s(x2), x3))
H(b, x1, s(x2), x3) → c3(F(x1, x1, s(x2), x3))
F(a(z0), a(z0), s(x1), x2) → c1(G(z0, a(z0), s(x1), x2))
S tuples:
G(x0, x1, s(x2), x3) → c2(H(x0, x1, s(x2), x3))
H(b, x1, s(x2), x3) → c3(F(x1, x1, s(x2), x3))
F(a(z0), a(z0), s(x1), x2) → c1(G(z0, a(z0), s(x1), x2))
K tuples:none
Defined Rule Symbols:
f, g, h, a
Defined Pair Symbols:
F, G, H
Compound Symbols:
c1, c2, c3
(19) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use instantiation to replace
F(
a(
x0),
x1,
s(
x2),
x3) →
c1(
G(
x0,
x1,
s(
x2),
x3)) by
F(a(z0), a(z0), s(x1), x2) → c1(G(z0, a(z0), s(x1), x2))
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a(z0), z1, s(z2), z3) → f(a(b), z1, z2, g(z0, z1, s(z2), z3))
g(z0, z1, z2, z3) → h(z0, z1, z2, z3)
h(b, z0, z1, z2) → f(z0, z0, z1, z2)
a(b) → c
Tuples:
G(x0, x1, s(x2), x3) → c2(H(x0, x1, s(x2), x3))
H(b, x1, s(x2), x3) → c3(F(x1, x1, s(x2), x3))
F(a(z0), a(z0), s(x1), x2) → c1(G(z0, a(z0), s(x1), x2))
S tuples:
G(x0, x1, s(x2), x3) → c2(H(x0, x1, s(x2), x3))
H(b, x1, s(x2), x3) → c3(F(x1, x1, s(x2), x3))
F(a(z0), a(z0), s(x1), x2) → c1(G(z0, a(z0), s(x1), x2))
K tuples:none
Defined Rule Symbols:
f, g, h, a
Defined Pair Symbols:
G, H, F
Compound Symbols:
c2, c3, c1
(21) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
G(
x0,
x1,
s(
x2),
x3) →
c2(
H(
x0,
x1,
s(
x2),
x3)) by
G(b, z1, s(z2), z3) → c2(H(b, z1, s(z2), z3))
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a(z0), z1, s(z2), z3) → f(a(b), z1, z2, g(z0, z1, s(z2), z3))
g(z0, z1, z2, z3) → h(z0, z1, z2, z3)
h(b, z0, z1, z2) → f(z0, z0, z1, z2)
a(b) → c
Tuples:
H(b, x1, s(x2), x3) → c3(F(x1, x1, s(x2), x3))
F(a(z0), a(z0), s(x1), x2) → c1(G(z0, a(z0), s(x1), x2))
G(b, z1, s(z2), z3) → c2(H(b, z1, s(z2), z3))
S tuples:
H(b, x1, s(x2), x3) → c3(F(x1, x1, s(x2), x3))
F(a(z0), a(z0), s(x1), x2) → c1(G(z0, a(z0), s(x1), x2))
G(b, z1, s(z2), z3) → c2(H(b, z1, s(z2), z3))
K tuples:none
Defined Rule Symbols:
f, g, h, a
Defined Pair Symbols:
H, F, G
Compound Symbols:
c3, c1, c2
(23) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)
Removed 3 of 3 dangling nodes:
G(b, z1, s(z2), z3) → c2(H(b, z1, s(z2), z3))
F(a(z0), a(z0), s(x1), x2) → c1(G(z0, a(z0), s(x1), x2))
H(b, x1, s(x2), x3) → c3(F(x1, x1, s(x2), x3))
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a(z0), z1, s(z2), z3) → f(a(b), z1, z2, g(z0, z1, s(z2), z3))
g(z0, z1, z2, z3) → h(z0, z1, z2, z3)
h(b, z0, z1, z2) → f(z0, z0, z1, z2)
a(b) → c
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
f, g, h, a
Defined Pair Symbols:none
Compound Symbols:none
(25) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(26) BOUNDS(O(1), O(1))